perm filename FOO.PUB[LSP,JRA]3 blob
sn#110748 filedate 1974-07-09 generic text, type T, neo UTF8
.SS(Towards a Mathematical Semantics)
In {yonss(*)} we informally introduced some ideas about proving properties
of programs. We would now like to expand on this idea of introducing
mathematical rigor into the discussion of programming languages. Though firm
technical basis can be extablished for the following discussion, we
wish to proceed at an intuitive level and hopefully arouse curiosity
without damaging the underlying theory.
First, why worry about foundational and theoretical work at all? Programmning,
it is said, is an art and art needs no formalizing. Indeed, but there is some
science in Computer Science and %2that%* part can be analyzed.
The description of LISP which we have given so far is classified as ⊗→operational↔←.
That means our informal description of LISP and our later description of the LISP
interpreter are couched in terms of "how does it work (operate)". Indeed
the whole purpose of %3eval%* was to describe explicitly what is to happen
when a LISP expression is to be evaluated. We have seen *** that discussion
of evaluation schemes is non-trivial; and that order of evaluation can effect the
outcome ***. One difficulty with the opertational approach is that it (frequently)
specifies too much. Many time the order of evaluation is immaterial.
There is another way of looking at LISP expressions called ⊗→denotational↔← semantics.
We could say that a LISP form %2denotes%* some sexpression (or is undefined) just
as we could say that 2+2 denotes 4. The scheme which we use to evaluate the expression
is irrelevant; there is some object which our expression denotes and the process
which we use to discover that object is irrelevant. Mathematically speaking then
we have an abstract domain and expressions in our language denote objects in
our domain; the order of evaluation, indeed the %2process%* of evaluation, does not
concern us.
Let us begin to relate this discussion to LISP. Clearly, our domain will include
the S-expressions since %2most%* LISP expressions %2denote%* Sexprs. However, we
must include more; many of our functions are partial functions. Our domain
must then include a denotation for %3undefined%*. We will use the symbol %8U%*.